n:. upto(n)  n List 

latex

Definitions	S  T, ij, , if b t else f fi, i=j, as @ bs, upto(n), {i..j}, A, False, P  Q, i  j < k, P & Q, AB, x:A. B(x), t  T
Lemmas	le wf, append wf, int seg wf, eq int wf, ifthenelse wf, nat wf, nat properties, ge wf